Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
p
(
s
(x))
→ x
2:
fac
(
0
)
→
s
(
0
)
3:
fac
(
s
(x))
→
times
(
s
(x),
fac
(
p
(
s
(x))))
There are 2 dependency pairs:
4:
FAC
(
s
(x))
→
FAC
(
p
(
s
(x)))
5:
FAC
(
s
(x))
→
P
(
s
(x))
The approximated dependency graph contains one SCC: {4}.
Consider the SCC {4}. The usable rules are {1}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.01 seconds) --- May 3, 2006